Step of Proof: assert_elim
9,38
postcript
pdf
Inference at
*
1
2
I
of proof for Lemma
assert
elim
:
1.
ff
ff = tt
latex
by InstLemma `assert_of_ff` []
latex
1
:
1:
2.
(
ff)
1:
ff = tt
.
Definitions
A
Lemmas
assert
of
ff
origin
ff
ff = tt
by InstLemma `assert_of_ff` []
1:
1: 2. 
(ff)
1: ff = tt
.ff
ff = tt
by InstLemma `assert_of_ff` []
1:
1: 2. (ff)
1: ff = tt
.A